Issue2024-fun.agda:3,17-20
Not in scope:
  Foo at Issue2024-fun.agda:3,17-20
when scope checking Foo
